\chapter{面向大规模网络的数据平面一致性快速验证研究}
\label{cha:consistency}
本章主要研究面向大规模网络的数据平面一致性快速验证。首先，通过分析已有研究工作发现了在大规模网络中普遍存在的“长尾到达”现象，提出了数据平面验证的一致性验证和快速验证问题，并提出数据平面验证的CWT理论。然后，探讨了“长尾到达”所涉及的更新完成状态不确定性和数据平面更新异步性等挑战。接着，提出了面向大规模网络的数据平面一致性快速验证方法CE2D。作为Flash的验证过程模块，CE2D将数据平面更新划分为不同的纪元（Epoch），并提出了基于递减图查询的增量式验证方法。最后，实验表明，相对于已有工作，CE2D能够将验证速度提高1,163倍。


\cref{fig:ce2d-outline} 列出了面向大规模网络的数据平面一致性快速验证研究路径。首先在\cref{sec:ce2d-background}中提出大规模网络中的数据平面验证背景，在\cref{sec:ce2d-problem}中提出数据平面一致性快速验证所研究的问题，并分析直观思路，在\cref{sec:ce2d-challenge}中提出基于直观思路解决大规模网络一致性验证问题所面临的挑战，在\cref{sec:ce2d-cdm}和\cref{sec:ce2d-dqg}针对挑战提出相应的解决方案，并在\cref{sec:ce2d-eval}中对所提出的解决方案进行实验验证。

\begin{figure}
  \centering
  \includegraphics[width=\linewidth]{figures/consistency/outline.pdf}
  \caption{面向大规模网络的数据平面一致性快速验证研究路径}
  \label{fig:ce2d-outline}
\end{figure}

\section{面向大规模网络的数据平面一致性快速验证研究背景}
\label{sec:ce2d-background}
为了实现可验证路由编程的高效验证过程，需要在数据平面模型上应用相应的算法，而数据平面验证过程主要是在数据平面模型上采用相应的图算法进行验证，如可达性需求可以通过深度遍历方法进行验证，虽然\cref{cha:model}的工作实现了高效地数据平面模型构建过程，然而，在实际情况中，直接在数据平面模型上进行图算法验证仍然存在问题。


\textbf{数据平面更新的长尾到达（Long-tail arrival）现象。}虽然数据平面模型快速构建过程能够很好地应对大规模网络中的更新风暴问题，然而，在大规模网络中还存在另外一种极端情况，即某些网络设备的FIB更新需要很长时间才能到达验证系统，本文将这种情况称为“长尾到达”（Long-tail arrival）。造成“长尾到达”的原因可能有多种，比如网络设备路由软件故障导致路由计算无法收敛，资源争用导致FIB更新过程缓慢，不稳定链路导致FIB更新阻尼，或者汇聚拥塞（Incast conjestion）~\cite{alizadeh2010data}导致数据包丢失。

在“长尾到达”情况下，由于系统没有收集到所有数据平面更新，所以验证系统构建的数据平面模型是不完整的。目前的数据平面验证系统通常采用以下两种方式来应对这种情况：（1）直接在不完整的数据平面模型上进行验证，这种方式可以在部分数据平面更新收集完成后就开始验证，从而尽早发现潜在的网络错误。然而，由于数据平面模型的不完整性，可能会导致验证结果的不准确性。另一种常见的方式是（2）等待所有数据平面更新收集完成后再进行验证。这种方式可以确保验证系统使用完整的数据平面模型进行验证，从而得到更准确的结果。然而，等待所有数据平面更新收集完成可能会导致验证效率低下和响应时间延迟，特别是在存在“长尾到达”的情况下，某些设备的更新可能会出现延迟，导致等待时间较长。在这种情况下，验证系统需要花费大量时间等待数据平面更新完成，从而导致验证结果的延迟。本文通过具体例子分别分析这两种方式存在的问题。

\textbf{在不完整的数据平面模型上进行验证导致错误的验证结果。} 由于FIB收集的异步特性，验证系统收到的FIB更新顺序可能与当前数据平面更新的实际顺序不一致，从而导致错误的验证结果。如图~\ref{fig:consistency-example} 所示为一个包含三个交换机的网络，每个交换机当前的FIB在FIBs表格中给出，图最右边为当前数据平面对于包头空间10.0.0.0/8的等价类的数据平面模型。当链路S2-S3失效时，如图~\ref{fig:consistency-example-incorrect} 所示，路由软件会重新计算各个网络设备的FIB，其中S1和S2分别将包头空间属于10.0.0.0/8的数据包转发到S3和S1（如图~\ref{fig:consistency-example-incorrect} 中FIBs表中绿色部分所示），为了保证数据平面没有转发循环存在，网络控制平面会先更新S1再更新S2。然而，不同设备的FIB更新会异步地发往验证系统，导致验证系统可能会先收到S2的更新再收到S1的更新。在收到S2的更新后，对应的更新后的数据平面模型如图~\ref{fig:consistency-example-incorrect} 最右边所示，如果验证系统此时在该数据平面模型上进行验证，会发现S1和S2之间存在转发循环，但实际上数据平面并不存在这样的转发循环，从而导致了错误的验证结果。

\begin{figure}[htp]
  \centering
  \includegraphics[width=\textwidth]{consistency/example.pdf}
  \caption{示例网络及其FIB和数据平面模型}
  \label{fig:consistency-example}
\end{figure}

\begin{figure}[htp]
  \centering
  \includegraphics[width=\textwidth]{consistency/example-incorrect.pdf}
  \caption{示例网络链路状态变化导致FIB和数据平面模型更新}
  \label{fig:consistency-example-incorrect}
\end{figure}

\textbf{等待所有数据平面更新收集完成后再验证导致验证效率低下。} 在存在数据平面更新“长尾到达”现象的情况下，等待所有数据平面更新收集完成后再验证会导致验证结果严重延迟。如图~\ref{fig:consistency-example-long-tail} 所示，展示了OpenR设备的端口不稳定情况下发生状态跳变导致FIB计算阻塞的示例。图中的横轴表示状态变化次数，纵轴表示从第一次变化开始到收到该设备的FIB更新所经过的时间。可以观察到，随着状态变化次数的增加，FIB计算的延迟呈指数增长，当状态变化次数达到8次或更多时，FIB计算的延迟达到最大值60秒。如果验证系统等待接收到该设备的FIB更新后才进行验证，那么验证结果将在60秒之后才能得出，这将导致验证系统的效率低下。

\begin{figure}[htp]
  \centering
  \includegraphics[width=0.75\textwidth]{consistency/long_tail.pdf}
  \caption{OpenR设备由于端口状态跳变导致FIB计算阻塞}
  \label{fig:consistency-example-long-tail}
\end{figure}

那么，是否存在一种有效的方式实现\textbf{在未收集到全部设备FIB更新的情况下，得到与收集到全部FIB更新后一致的验证结果。} 对于该问题，本文有以下观察：当一个网络事件导致网络数据平面配置更新时，如果验证系统已经收到某些设备的全部更新，在基于这些设备构成的数据平面模型上进行验证，验证结果与收集到完整数据平面更新的结果一致，本文将这个过程称为“提前验证”。例如，在两个设备之间检测到的转发环路的存在与否与其他设备的数据包转发方式无关。因此，只要这两个设备处于收敛状态（即不更新其FIB，除非网络状态发生变化），就可以报告此错误，而无需其他设备的FIB信息。所以，为了应对大规模网络中的“长尾到达”现象，本文进行了面向大规模网络的数据平面一致性快速验证研究。



% Flash 基于这一观察构建，并引入了一种系统机制，确保 Flash \textit{始终在一致的网络状态下进行提前验证}。具体而言，Flash 使用\emph{时期（epochs）}来区分从不同网络状态计算的FIB更新，并将提前验证应用于在同一时期内从相同网络状态计算的\emph{同步}设备的模型上。Flash 捕获了时期的偏序关系，以实现高效的调度。然后，本文利用自动机理论开发了新颖的算法，实现高效的提前验证。

% 造成上述问题的原因在于数据平面的更新过程没有与数据平面模型的更新过程同步，其过程属于最终一致性范畴，然而更新过程并不能保证二者完全一致，导致数据平面模型更新过程的过渡状态不能真实反映数据平面的状态。


\section{面向大规模网络的数据平面一致性快速验证问题描述}
\label{sec:ce2d-problem}

% \subsection{一致性数据平面模型}
% 数据平面模型是根据数据平面构建，模型的特性依赖于数据平面特性，所以，一致性的验证结果依赖于一致性的数据平面模型。对于一个数据平面$DP(G,\mathbb{T})$，$\mathbb{T}$是控制平面根据网络状态（如网络拓扑、地址分配等）计算得出，例如当前广泛使用的IGP控制平面软件OSPF、ISIS和OpenR~\cite{meta2023openr}，各网络设备通过相应的协议在本地维护网络状态，基于本地状态计算路由规则。给定一个网络设备$d$，其维护的网络状态为$d.state$，令$T_d = CP_d(d.state)$表示设备$d$根据网络状态计算得到其数据平面配置$T_d$，$state(T_d) = d.state$表示计算$T_d$所使用的网络状态，定义一致性数据平面如下：
% \begin{definition}
%   \textbf{一致性数据平面}。给定一个数据平面$DP(G,\mathbb{T})$，如果$\forall T_i,T_j \in \mathbb{T}: state(T_i) = state(T_j)$，则称数据平面$DP$为一致性数据平面。
% \end{definition}

% 显而易见的是，如果一个数据平面处于收敛状态，那么该数据平面一定满足一致性。相应地，数据平面模型的一致性定义如下：
% \begin{definition}
%   \textbf{一致性数据平面模型}。令$M = model(DP)$表示数据平面模型$M$根据数据平面$DP$构建，如果$DP$为一致性数据平面，则$M$为一致性数据平面模型。
% \end{definition}

% 例如，图~\ref{fig:consistency-example-incorrect} 所示的数据平面模型所依赖的数据平面具有两种网络状态，即S1-S2的失效与否，所以该数据平面模型不满足一致性，这也是系统输出了错误的验证结果的原因。

% \subsection{数据平面一致性提前验证}

为了实现“长尾到达”情况下的快速验证，需要能够在未获取到所有设备更新的情况下“提前”知道最终验证结果。同时，也需要相应的增量式验证算法来实现数据平面增量式验证。对于一致性验证，首先定义数据平面验证需求模型，数据平面需求描述了网络处理数据包的过程约束，比如按照某个特定的路径转发，具体描述如下。

\begin{definition}
  \textbf{网络路径($\pi$)。} 一个网络路径$\pi$为一个网络链路构成的有序序列$\pi = \{l_1, l_2,...,l_N\}$，其中$l_i \in L$，$N$为该路径长度，且相邻链路必须连接到同一个设备以保证路径连通，即$\forall i \in [1, N-1]: dstd(l_i) = srcd(l_{i + 1})$。
\end{definition}

需要指出的是，如果$srcd(l_1) \in term(D)$且$dstd(l_N) \in term(D)$，本文称路径$\pi$是一条端到端的路径（End-to-end path）。如果网络中不存在多链路（multi-link）情况，网络路径可以等价的表示为一个设备有序序列$\pi=\{d_1,d_2,...,d_N\}$，其中$d_i = dstd(l_i)$，从而能够更精简地表达一个路径。另外，本文用$\Pi \subseteq L^*$表示网络中的路径集合。

\begin{definition}
  \textbf{数据平面需求（$\rho$）。} 数据平面需求为一个元组$\rho = \langle d, h, \pi \rangle$，其中$d \in term(D)$为一个网络设备，$h$为一个数据包头，$\pi=\{l_1,...,l_N\}$为一条网络路径，且$d = srcd(l_1)$。对于一个数据平面需求$\rho$的语义为：从设备$d$出发且包头为$h$的数据包，网络需要按照路径$\pi$对该数据包进行转发。
\end{definition}

值得注意的是，已有工作如Merlin~\cite{soule2014merlin}和Propane~\cite{beckett2016don}等使用正则表达式方式表示路径需求，对于正则形式路径的需求依然可以等价的表示为多个满足正则条件的路径，上述数据平面需求抽象仍然可以作为基础结构表示这些需求。在本文实际系统中，也使用正则形式的路径需求，但并不打破上述数据平面需求抽象的定义。

针对数据平面一致性验证，令 $M_K$ 表示经过了 $K$ 次更新的数据平面模型，$M_k$ 表示仅经过了 $k \le K$ 次更新的数据平面模型。令 $ver$ 为需求检测函数，该函数以网络需求 $\rho$ 和模型 $M_k$ 为输入。由于 $M_k$ 只有部分信息网络数据平面信息，所以 $ver(\rho, M_k)$ 可能给出明确结果（即满足/不满足）或未知结果。

\begin{definition}
\label{def:ced}
\textbf{数据平面一致性验证}。对于一个网络需求 $\rho$，对一个数据平面模型 $M$ 和 $K$ 个 $M$ 上的任意更新，如果 $\exists k \le K$, $ver(\rho, M_k)$ 能够给出明确结果，而且 $ver(\rho, M_k) \equiv ver(\rho, M_{k+1}) \equiv ... \equiv ver(\rho, M_K)$，则 $ver$ 实现了对 $\rho$ 的一致性提前验证。
\end{definition}

\begin{figure}
  \centering\includegraphics[width=0.55\linewidth]{figures/consistency/cwt.png}
	\caption{数据平面验证的CWT理论}
  \label{fig:ce2d-cwt}
\end{figure}

\textbf{数据平面验证的CWT理论。} 为了实现一致性验证，同时尽可能验证更多的设备数据平面，且尽可能提前验证时机，本文引入了数据平面的整体性（Wholeness）和及时性（Timeliness）的概念。其具体定义如下：


\begin{definition}
  \textbf{数据平面验证的整体性。}数据平面验证的整体性表示验证过程涵盖所有设备，即给定一个网络$G(D,L)$以及验证系统输入的数据平面模型$M\langle V,A,\Sigma,\delta \rangle$，其中$V = D$。
\end{definition}
例如，在检测网络循环的过程中，需要对所有设备FIB状态构成的数据平面模型进行检测。

\begin{definition}
  \textbf{数据平面验证的及时性。}数据平面验证的及时性表示在未收集到全部设备FIB更新时就能够给出验证结果，即对于一个发生$K$个更新的网络，验证系统能够在收到$k < K$次更新时给出明确验证结果。
\end{definition}

然而，本文提出了以下理论，即数据平面验证系统无法同时满足一致性、整体性和及时性，如\cref{fig:ce2d-cwt}所示。验证系统最多只能同时满足其中两个性质。本文将该理论称为数据平面验证的CWT理论，其具体定义和证明如下：

\begin{theorem}
  \textbf{数据平面验证的CWT理论。}在具有多个设备的网络中，如果发生“长尾到达”现象，数据平面验证系统不能同时满足一致性（Consistency）、整体性（Wholeness）和及时性（Timeliness）。
\end{theorem}

\begin{proof}
  假设存在一个验证系统同时满足一致性、整体性和及时性，考虑图 \ref{fig:ce2d-cwt-proof} 中的案例，其中绿色框表示已收集的FIB更新，红色框表示未收集的FIB更新，当设备C的FIB更新未收集完成，构建的数据平面模型如\cref{fig:ce2d-cwt-proof1}所示（示例考虑10.0.0.0/8的等价类），由于系统满足整体性和及时性，此时在该数据平面模型上进行验证会得到A-B-C之间存在路由循环。然而，当所有设备的FIB更新收集完毕时，如\cref{fig:ce2d-cwt-proof2}所示，会发现该循环并不存在，所以打破了一致性要求。为了进一步将该例子一般化，考虑设备B和C，如果C的默认路由是发往B，则B-C之间会在C未收集完FIB更新时验证出环路，而“长尾到达”的网络中出现上述情况的可能性存在，同时具有多个设备的网络中的设备数量必定大于2，所以在这种情况下数据平面验证系统始终不能同时满足一致性、整体性和及时性。
\end{proof}

\begin{figure}[htbp]
  \centering
  \begin{subfigure}[t]{0.44\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/consistency/cwt-proof1.pdf}
    \caption{设备C的FIB更新未收集完毕}
    \label{fig:ce2d-cwt-proof1}
  \end{subfigure}
  \hspace{1em}
  \begin{subfigure}[t]{0.44\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/consistency/cwt-proof2.pdf}
    \caption{所有设备的FIB更新已收集完毕}
    \label{fig:ce2d-cwt-proof2}
  \end{subfigure}
  \caption{数据平面验证的CWT理论证明示例}
  \label{fig:ce2d-cwt-proof}
\end{figure}

% \todo{delete}
% 为了保证所构建的数据平面模型与真实数据平面一致，本文需要保证1）数据平面模型所对应的数据平面在网络中真实存在；2）数据平面模型的变化顺序与数据平面的变化顺序一致。具体而言，令$DP(M)$表示数据平面模型$M$所对应的数据平面，且$DP_i \prec DP_j$表示数据平面状态$DP_i$先于$DP_j$，本文定义数据平面一致性如下：
% \begin{definition}
%   \textbf{完全（强）一致性数据平面模型}。给定一个数据平面$DP$，当发生网络事件时（如链路失效），由于网络设备收到该事件的时间存在差异，数据平面按照时间序列$\Psi = \{DP_1,...,DP_k\}$发生$k$次更新，最终被更新为$DP_k$。同时，数据平面模型也按照一定的时间顺序更新为$\{M_1,...,M_n\}$。如果$\forall i < j \in \{1,...,n\}: DP(M_i) \in \Psi, DP(M_j) \in \Psi, DP(M_i) < DP(M_j)$，则本文称数据平面模型与数据平面一致。
% \end{definition}

\begin{table}[h]
  \center
  \caption{已有系统类型分析}
  \label{tab:cwt-analysis}
  \begin{tabular}{|c|c|c|c|c|c|c|}
    \hline
    \emph{系统名称}
    & \emph{一致性(Consistency)}
    & \emph{整体性(Wholeness)}
    & \emph{及时性(Timeliness)}
    \\\hline
    ConfigChcker~\cite{al-shaer2009network} & N & Y & N
    \\\hline
    FlowChcker~\cite{al-shaer2010flowchecker} & N & Y & N
    \\\hline
    HSA~\cite{kazemian2012header} & N & Y & N
    \\\hline
    NetPlumber~\cite{kazemian2013real} & N & Y & Y
    \\\hline
    Veriflow~\cite{khurshid2012veriflow} & N & Y & Y
    \\\hline
    APV~\cite{yang2016realtime} & N & Y & Y
    \\\hline
    APT~\cite{yang2017scalable} & N & Y & Y
    \\\hline
    DeltaNet~\cite{horn2017deltanet} & N & Y & Y
    \\\hline
    APKeep~\cite{zhang2020apkeep} & N & Y & Y
    \\\hline
    Libra~\cite{zeng2014libra} & N & Y & Y
    \\\hline
    RCDC~\cite{jayaraman2019validating} & Y & N & N
    \\\hline
    Coral~\cite{xiang2023centralized} & N & N & Y
    \\\hline
  \end{tabular}
\end{table}

\cref{tab:cwt-analysis}列出了主要的已有数据平面验证系统类型，可以发现大部分均实现为WT系统，比如NetPlumber~\cite{kazemian2013real}每当收到并处理完一个数据平面更新时，立即触发验证过程。RCDC~\cite{jayaraman2019validating}虽然实现了一致性验证，它实现一致性的原因在于其默认网络运行固定的协议，且收集并处理完单个设备的完整更新后进行验证，然而该过程牺牲了整体性和及时性，在“长尾到达”情况下无法快速给出验证结果。

% \subsection{数据平面一致性快速验证主要研究问题}
根据数据平面验证的CWT理论，数据平面验证系统的性质必须舍弃其一满足其二，已有工作如APKeep~\cite{zhang2020apkeep}、DeltaNet~\cite{horn2017deltanet}、Veriflow~\cite{khurshid2012veriflow}等均在数据平面更新发生后立即进行满足整体性的验证，其构建的验证系统为WT系统，牺牲了一致性，可能导致大量的假阳性（False-positive）错误报告。然而，对于现代大规模高速网络来说，更需要的是能够在最快的时间给出明确一致的验证结果，从而尽可能将网络故障带来的损失降到最低。基于上述描述，本文旨在实现满足一致性和及时性的CT验证系统，具体需要研究的问题如下：

\textbf{P1:如何在长尾到达情况下实现一致性验证。} 数据平面更新的“长尾到达”导致了数据平面无法在短时间内收集到所有设备的全部FIB更新，所构建的数据平面模型长时间处于变化状态，在这样的情况下如何实现一致性验证是验证系统需要解决的关键问题之一。

为了实现在“长尾到达”情况下的一致性快速验证，需要设计实现满足一致性和及时性的CT（Consistency, Timeliness）系统，直观思路是牺牲一定的整体性，验证部分设备，并确定合适的验证时机，通过增量式验证算法实现高效验证。

\textbf{I1: 只对FIB更新处理完毕的设备进行验证。}只对FIB更新处理完毕的设备进行验证意味着验证系统仅对那些FIB不再发生更新的设备进行验证。这种方法是为了确保在进行验证操作时，设备的数据平面状态已经确定，在这些设备上验证出现的\textbf{确定结果}不会因其他设备FIB的变化而改变，从而确保验证结果的一致性。以\cref{fig:ce2d-int-loop}所示的拓扑为例，图中不同颜色箭头表示不同的等价类，实线设备（S1/2/3）表示已收集且处理全部FIB更新的设备，虚线设备（S4/5/6）表示未收集完全部FIB更新的设备，此时验证系统对S1/2/3进行验证时会发现一个循环（绿色箭头）而该循环不会因S4/5/6上的FIB变化而被打破。

\begin{figure}[htbp]
  \centering
  \begin{subfigure}[]{0.44\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/consistency/intuition-loop.pdf}
    \caption{设备S1/2/3的全部更新已收集}
    \label{fig:ce2d-int-loop}
  \end{subfigure}
  \hspace{1em}
  \begin{subfigure}[]{0.44\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/consistency/intuition-sync.pdf}
    \caption{设备S4的全部更新已收集}
    \label{fig:ce2d-int-sync}
  \end{subfigure}
  \caption{数据平面一致性快速验证基本思路示例}
\end{figure}

\textbf{P2:如何在长尾到达情况下实现快速验证。} 由于“长尾到达”导致数据平面模型长时间处于变化状态，每次数据平面模型发生变化都进行重复验证会导致极大的计算开销，如何在“长尾到达”情况下实现快速验证是实现满足及时性的数据平面验证系统的关键问题之一。


\textbf{I2: 每当有设备FIB更新处理完毕则立即验证。}为了实现数据平面验证系统的及时性，在“长尾到达”情况下需要尽可能提前进行验证，基本思路是在I1（只对FIB更新处理完毕的设备进行验证）的基础上，每当有设备FIB更新处理完毕则立即验证，这种验证策略可以迅速捕捉到数据平面更新所引起的任何错误。在\cref{fig:ce2d-int-sync}所示的例子中，S1/2/3的FIB更新已全部处理完毕，当S4的FIB更新处理完毕时，立即对S1/2/3/4所构成的数据平面模型进行验证，假设需求为S1-S5的可达性验证，则可以立即给出S1-S5可达的确定性验证结果（S1-S2-S4-S5），而该结果不会因为S5/6上的FIB变化而改变。对于可达性需求，一种简单高效的增量式验证方法是基于集合包含传递（Transitive Set-Containment）~\cite{ciesielski1997set}的算法，即若$Set_A$为设备$A$的可达设备集合，如果$B$可达$A$则$Set_A$同时为$B$的可达设备集合~\cite{xu2010graph}，随着设备FIB更新不断完成，通过集合合并不断迭代即可实现增量式可达性验证。

% \section{面向大规模网络的数据平面一致性快速验证基本思路}


\section{面向大规模网络的数据平面一致性快速验证的挑战}
\label{sec:ce2d-challenge}

虽然实现一致性快速验证的基本思路看起来简单，然而这些思路基于一个非常严格的设定，即设备的FIB更新已经完成，而实际网络中设备的FIB会不断发生变化，使得基本思路的实现面临巨大挑战。具体而言，实现面向大规模网络的数据平面一致性快速验证主要有以下挑战：


\textbf{C1: 设备FIB更新完成状态不确定性。}在实际网络中，由于网络状态（如拓扑、IP前缀）的变化，设备的FIB可能随时发生更新，所以无法确定网络设备FIB更新的完成状态，也就无法保证一个设备的FIB不再更新。以当前主流的开源路由软件FRR~\cite{FRR}为例，其FIB更新通过Zebra~\cite{zebra}提供的TCP流式接口发送给数据平面验证系统，验证系统在收到一系列FIB更新时无法判断是否还存在后续更新，导致设备FIB更新完成状态不确定。

\textbf{C2: 数据平面更新的异步性。}网络设备本身构成一个分布式系统，在动态路由协议（如OSPF）的加持下，不同设备的FIB根据其所获得的网络状态（如LSDB）异步更新并发送到验证系统，数据平面更新的异步性意味着不同网络设备的FIB更新顺序与验证系统收到的FIB更新顺序可能不一致，在这种情况下验证可能得到错误的验证结果。例如，在\cref{fig:model-inconsistent-dpm}三节点拓扑中，每个节点都有一个针对前缀10.0.0.0/8的转发规则，数据模型图如底部所示。当S1和S2之间的链路断开时，S2和S3将会更新它们的FIB，如绿色矩形所示。如果S3在S2之前更新它的FIB，网络中将不会出现环路。然而，如果由于更新收集的异步性或者收集S3的更新时发生了“长尾到达”情况，验证系统将先接收到来自S2的更新，将得到一个在S2和S3之间形成环路的转发图，然而很显然网络中并不存在这样的循环。

\begin{figure}
  \centering\includegraphics[width=\linewidth]{figures/consistency/inconsistent-dpm.png}
	\caption{数据平面更新的异步性导致错误的验证结果}
  \label{fig:model-inconsistent-dpm}
\end{figure}

\textbf{C3: 数据平面验证过程计算冗余。}为了保证数据平面验证的及时性，虽然I2（每当有设备FIB更新处理完毕则立即验证）的策略能够尽快地提前验证时机，且实现一致性验证，但在大规模网络中，大量网络设备可能在短时间内变为完成状态，每当有设备FIB更新处理完毕都触发验证的策略对验证算法的效率有较高要求。然而，I2中描述的增量式验证方法可能会产生大量冗余计算，尤其是在“扇出”网络（Fanout Network）中尤为明显。在\cref{fig:ce2d-cha-red}所示的案例中，验证需求为设备S到T的可达性，网络中除了设备A以外其他设备的FIB的更新均已完整收集且处理，然而，由于系统并不知道S到T的路径经过哪些设备，基于集合包含传递（Transitive Set-Containment）算法将计算所有FIB更新完成设备的可达设备集合，然而，该网络并没有从S到D/E/F/G的路径，导致对设备D/E/F/G的可达设备计算冗余。

% \textbf{C1:数据平面更新所对应的网络状态不确定性。}数据平面更新所对应的网络状态不确定性是指无法根据数据平面更新确定其对应的网络状态，在这种情况下验证可能得到错误的验证结果。例如，在\cref{fig:model-inconsistent-dpm}三节点拓扑中，每个节点都有一个针对前缀10.0.0.0/8的转发规则，数据模型图如底部所示。当S1和S2之间的链路断开时，S2和S3将会更新它们的FIB，如绿色矩形所示。如果S3在S2之前更新它的FIB，网络中将不会出现环路。然而，如果由于更新收集的异步性或者收集S3的更新时发生了“长尾到达”情况，验证系统将先接收到来自S2的更新，将得到一个在S2和S3之间形成环路的转发图，然而很显然网络中并不存在这样的循

\begin{figure}[htbp]
  \centering\includegraphics[width=0.7\linewidth]{figures/consistency/challenge-redundant.pdf}
	\caption{数据平面验证过程计算冗余示例}
  \label{fig:ce2d-cha-red}
\end{figure}

% \textbf{C2:数据平面模型的不完整性。}针对问题P2，“长尾到达”会导致数据平面不完整。如\cref{fig:model-incomplete-dpm}所示的例子，网络需求为B到A的可达性，其中S1和S3的数据平面更新被正常收集，而S2的数据平面更新发生了“长尾到达”，最后形成的数据平面模型如\cref{fig:model-incomplete-dpm}右上方所示。如果认为S2的数据平面配置为空，相当于S2将所有的数据包都丢弃，则形成的数据平面模型如图右下角所示，在该数据平面模型上验证会得到B到A不可达，显然这是一个错误的验证结果。另一方面，如果认为S2可以将数据包发往任意邻居，则构建的数据平面模型如图右下角所示，在该数据平面模型上验证会得到S2-S3之间存在循环，而实际网络中并不存在该循环。另外，如果等待所有数据平面更新收集完成后再验证导致验证结果的延迟，对于高速网络来说可能导致灾难性的后果。所以，数据平面模型的不完整性是实现“长尾到达”情况下的快速验证的挑战。

% \begin{figure}
%   \centering\includegraphics[width=\linewidth]{figures/consistency/challenge-incomplete.pdf}
% 	\caption{数据平面模型的不完整性}
%   \label{fig:model-incomplete-dpm}
% \end{figure}

% \begin{enumerate}
%   \item \textbf{如何区分数据平面更新所对应的网络状态。} 由于一致性提前验证依赖于一致性数据平面，而一致性数据平面的构建需要根据数据平面更新所对应的网络状态对数据平面更新进行划分和过滤，而当前已有网络设备所发送的FIB更新缺少其相关网络状态信息。
%   \item \textbf{如何在不完整的数据平面模型上进行增量式验证。} 由于数据平面往往是在一定时间段内逐步收敛，为了进一步提高验证效率，需要实现增量式的验证，从而进一步提高验证效率。
% \end{enumerate}

% 每个网络设备的FIB更新都有对应的时间，有了时间本文就能比较更新发生的先后顺序。如果是单个计算机内执行的事务，由于它们共享一个计时器，所以能够很容易通过时间戳来区分先后。但是，网络本身为一个分布式环境，通过时间戳的方式来区分先后并不可行。因为在分布式系统中的不同节点间保持它们的时钟一致并不容易。因为每个节点的CPU都有自己的计时器，而不同计时器之间会产生时间偏移，最终导致不同节点上面的时间不一致。也就是说如果A节点的时钟走的比B节点的要快1分钟，那么即使B先发出的消息（附带B的时间戳），A的消息（附带A的时间戳）在后一秒发出，A的消息也会被认为先于B发生。那么是否可以通过某种方式来同步不同节点的物理时钟呢？NTP就是常用的时间同步算法，但是即使通过算法进行同步，总会有误差，这种误差在某些场景下（如骨干网络实时网络验证）是不能接受的。

% \section{数据平面验证一致性问题相关工作}
% \subsection{顺序一致性方案}
% 分布式系统解决了传统单体架构的单点问题和性能容量问题，另一方面也带来了很多的问题，其中一个问题就是多节点的时间同步问题：不同机器上的物理时钟难以同步，导致无法区分在分布式系统中多个节点的事件时序。1978年Lamport在《Time, Clocks and the Ordering of Events in a Distributed System》中提出了逻辑时钟的概念，来解决分布式系统中区分事件发生的时序问题。

% 顺序一致性使用的是逻辑时钟来作为分布式系统中的全局时钟，进而所有进程也有了一个统一的参考系对读写操作进行排序，因此在任意时刻，数据平面及其模型的更新顺序是一样的。

% \section{基于Epoch的一致性数据平面模型设计}
% 为了实现一致的数据平面模型构建，数据平面验证系统需要满足以下要求：(1)能够识别来自相同网络状态计算的一致FIB更新；(2)能够识别潜在的收敛状态；(3)能够调度潜在收敛状态的一致FIB更新到同一验证器以提高效率和正确性。为此，本文设计了一种适用于多个路由协议的一致模型构建机制。在本章中，本文重点介绍广播状态同步协议，包括链路状态协议OSPF/ISIS和通用状态同步协议OpenR。

\section{基于一致性数据平面模型的一致性提前验证方法}
\label{sec:ce2d-cdm}

\subsection{一致性数据平面模型}
网络的数据平面由控制平面管理，而控制平面基于网络状态（如网络拓扑，路由配置等）生成数据平面配置。如OpenR，OSPF和ISIS等控制平面软件能够通过相应的协议发现网络拓扑，然后计算各个网络设备的数据平面配置。令$C_d(state_d)=R_d$为控制平面生成数据平面配置的函数，其中$state_d$为设备$d$所存储的网络状态，令$state_d = C_d^{-1}(R_d)$为$C_d$的反函数，则有如下定义：
\begin{definition}
  一致性数据平面模型(consistent data plane model)：给定一个数据平面配置$\mathcal{R}=\{R_1,...,R_N\}$，如果$\forall R_i, R_j \in \mathcal{R}: C_d^{-1}(R_i) = C_d^{-1}(R_j)$，则由$\mathcal{R}$构建的数据平面模型为一致性数据平面模型。
\end{definition}

\subsection{基于Epoch的一致性数据平面模型构建过程}

为了实现一致的数据平面模型构建，数据平面验证系统需要满足以下要求：(1)能够识别来自相同网络状态计算的一致FIB更新；(2)能够识别潜在的收敛状态；(3)能够调度潜在收敛状态的一致FIB更新到同一验证器以提高效率和正确性。为此，需要设计一种适用于多个路由协议的一致模型构建机制。在本章中，重点介绍广播状态同步协议下的一致性验证，包括链路状态协议OSPF，ISIS和通用状态同步协议OpenR。

网络的数据平面由控制平面生成，而控制平面基于网络状态（如网络拓扑，路由配置和链路权重等）生成数据平面配置。如OpenR和OSPF等控制平面软件通过邻居之间交换网络信息方法发现网络拓扑，然后各个设备分别独立计算各自的数据平面配置，本文将基于同一个网络状态计算出的数据平面配置称为一个纪元（Epoch），具体定义如下：
\begin{definition}
  \textbf{数据平面中的纪元（Epoch）}。一个数据平面Epoch为一个FIB集合$\{R_1,...,R_N\}$，且$\forall i, j \in \{1,...,N\}: C_d^{-1}(R_i) = C_d^{-1}(R_j)$，则称该FIB集合构成一个纪元（Epoch）。
\end{definition}

首先，Flash使用网络状态来表示路由软件用来计算转发规则的信息，如链路状态和前缀配置等。随着网络的变化，状态也会因不同事件（如链路故障）而发生变化。在同步状态协议中，状态更改会传播到整个网络。为了区分不同的状态，Flash使用纪元（Epoch）来划分不同网络状态计算的规则更新。具体来说，每个纪元表示全局网络状态的快照。

其次，Flash通过代理增强路由软件来识别与纪元一致的FIB更新。代理计算唯一的纪元标识符，并将标识符与根据状态计算的FIB更新相关联。为了保证调度的正确性，Flash要求代理和分发器之间的消息传递是串行的，即，来自同一设备的更新总是以与生成更新相同的顺序接收。但是，Flash对来自不同设备上的代理的消息没有限制。



\textbf{通过Epoch依赖跟踪识别潜在的收敛状态。}
由于 Flash 要求设备更新发送到分发器时有严格的顺序，如果分发器在设备 $i$ 上收到标记为 $t_1$ 的更新，然后收到标记为 $t_2$ 的更新，那么 $t_1$ 不是收敛状态。同样地，如果在设备 $j$ 上收到了 $t_2$，然后收到了 $t_3$，即使 $t_2$ 是设备 $i$ 上最近的标记，则可以推断 $t_2$ 也不是收敛状态。这在分布式系统中被称为“先于”关系，表示为 $t_1 \prec t_2$。Flash 维护每个设备的最新纪元标记和一个“活跃”纪元集合。一旦从设备 $i$ 接收到新的标记 $t_\text{new}$，其旧标记为 $t_i = t_\text{old}$，Flash 从活跃集合中删除 $t_\text{old}$ 并用 $t_\text{new}$ 替换 $t_i$。如果 $t_\text{new}$ 没有被标记为非活跃（由另一个设备标记），Flash 将 $t_\text{new}$ 添加到活跃集合中。一个标记在活跃集合中的纪元就是一个潜在的收敛状态。

\textbf{一致性数据平面更新分发过程。}
由于更新与纪元标记相关联，Flash 维护一个从纪元标记到验证器的映射。具体而言，在从设备接收到带有新纪元标记 $t$ 的更新时，Flash 首先将更新追加到设备的更新队列中，并检查 $t$ 是否在活跃集合中。如果 $t$ 不在活跃集合中，表示将来会有相同设备的更新，不需要采取进一步的操作。否则，如果 $t$ 在活跃集合中，Flash 查找（如果不存在则创建）$t$ 对应的验证器，并将设备的更新队列中的更新传递给该验证器。在实践中，为了避免由于控制平面错误或不稳定链路的不当处理而导致验证器快速创建，Flash 可能需要采用退避机制来避免大量无效验证器的创建。

\textbf{基于一致性数据平面模型的一致性验证过程。}实现一致性验证的核心思想是在一致数据平面模型上进行验证。在\cref{fig:model-consistent-model}所示的例子中，当两个链路S1-S2和S1-S3在短时间内（t0时刻）失效时，图中使用时间线来展示一个FIB更新的示例。在该案例中，各个设备可能会看到不同的网络状态，并根据它们的本地视图生成FIB更新，具体来说，各个设备可能有三种网络状态：1）S1-S2失效，2）S1-S3失效，以及3）S1-S2和S1-S3都失效。对于每个网络状态，系统分别构建相应的数据平面模型，属于同一个状态的数据平面更新被应用于相同网络状态的数据平面模型。当来自一个设备的属于一个网络状态的更新都接收到时，将这些更新应用于对应的模型，并将设备标记为已同步（Synchronized node），否则节点被标记为未同步（Unsynchronized node）。对于验证过程，只需要遍历已同步节点，由于已同步节点具有相同状态，所以验证的结果符合一致性。

\begin{figure}
  \centering\includegraphics[width=\linewidth]{figures/consistency/epoch.png}
	\caption{一致性数据平面模型构建示例}
  \label{fig:model-consistent-model}
\end{figure}

\section{基于一致性数据平面模型的增量式验证方法}
\label{sec:ce2d-dqg}

% \todo{对于冲突的需求只需要验证一个}

\subsection{基于递减图查询的增量式验证}
对常规需求执行一致的提前验证，包括路由、最短路径、任播和组播等，CE2D利用自动机理论 \cite{lewis1998elements}，将该问题转化为基于递减的验证图上的增量可达性查询问题 \cite{hanauer2020fully}。

\textbf{网络需求的乘积图（Product graph）表示。}
对于每个数据包空间 $H$ 和源节点集合 $srcs$，CE2D将网络拓扑和需求表达式自动机的交叉积自动机 $G_p$ 作为网络需求的表达形式 \cite{lewis1998elements, soule2014merlin, beckett2016don, hsu2020contra}，本文将该乘积图称为“验证图”。初始验证图包含满足以下两个条件的 $G$ 中的所有路径：1）从 $srcs$ 开始；2）路径构成的设备序列匹配需求中的正则表达式。

考虑\cref{fig:model-pg}中的网络和需求。要求子空间 $h$ 中进入 $S$ 的数据包必须沿着穿过 $W$ 和 $Y$ 中的一个节点的简单路径到达 $D$。\cref{fig:model-pg}右上侧显示了网络路径需求正则表达式的自动机结构，图下方显示了具有初始状态 $S1$ 和接受状态 $D1$ 的验证图。

\begin{figure}
  \centering\includegraphics[width=0.95\linewidth]{figures/consistency/pg.pdf}
	\caption{网络需求的乘积图表示}
  \label{fig:model-pg}
\end{figure}

基于验证图，验证需求表达式等价于在验证图中找到能够到达接受状态的路径。具体而言，如果存在一条只由同步节点组成的路径，则网络存在满足需求表达式的路径。如果存在一条只由同步节点到达拒绝状态的路径，则需求表达式不满足。否则，验证结果为“未知”。

\begin{theorem}
  如果数据平面模型$M_k$是一致性数据平面模型，令$ver_r$为基于递减图查询的验证函数，对于任意正则表达式类型的需求$\rho$，当$ver_r(M_k, \rho)$能够得到明确的结果，则$ver_r$实现了一致性提前验证。
\end{theorem}

\begin{proof}
  如果 $\var{ver}_r$ 不能实现一致性提前验证，那么根据定义~\ref{def:ced}，存在 $k' > k$ 使得 $\var{ver}_r(M_k, \rho) \neq \var{ver}_r(M_{k'}, \rho)$。这意味着在应用了 $k'$ 次更新后，检测结果发生了变化。由于 $\var{ver}_r$ 只有两种情况会得到明确结果：1）路径经过的节点都为已同步状态，或2）不存在满足验证图的路径。改变结果的唯一方法是更新已同步节点的 FIB。然而，$M_k$ 是一个保证在同步节点上没有更新的一致模型，因此不存在这样的 $k'$。
\end{proof}

\textbf{递减更新和可达性查询。}
随着更多节点被同步，网络中符合该网络需求的可能路径集合单调递减。考虑图 \ref{fig:model-pg} 中的示例，在收到“更新 1”之后，如图 \ref{fig:cmc-example}所示，验证图仅包含绿色区域中的节点和边。在进一步收到“更新 2”后，$G_P$ 中不存在有效路径，这意味着无论通过其他任意设备以任意方式转发 $h$，都无法满足图 \ref{fig:model-pg} 中的需求。在这样的递减图中（即边始终被删除，但从不被添加），可达性查询具有恒定的时间复杂度 \cite{hanauer2020fully}。



\begin{figure}[ht]
  \center
  \includegraphics[width=0.95\textwidth]{figures/consistency/dqg.pdf}
  \caption{递减图查询示例}
  \label{fig:cmc-example}
\end{figure}

基于正则表达式需求的快速、一致性提前验证的基本伪代码如\Cref{alg:early-reg}所示。该算法维护一个全局数据结构\emph{ecTable}，用于存储每个等价类的乘积图。初始时，它包含一个条目，其等价类匹配所有数据包头，并且乘积图是完整的（L1）。一旦新的模型准备好，算法就会遍历所有等价类，更新它们的乘积图并验证可达性（L6-16）。具体而言，它首先检查等价类$\var{ec}$的乘积图是否已存在。如果不存在，则$\var{ec}$从旧的等价类$\var{ec}^\prime$中拆分出来（L9-10），算法复制$\var{ec}^\prime$的乘积图，并为$\var{ec}$创建一个新的条目\footnote{该过程总是正确的，因为在每次更新时，FIB更新属于一组新同步的节点，即旧模型上这些节点的输出是相同的。因此，一个旧的等价类要么映射到一个新的等价类（如果在数据平面模型更新中存在一个具有相同谓词的条目），要么被拆分为多个等价类。}。然后，算法通过删除与$\var{ec}$在每个新同步节点$v$上的动作不一致的边来更新$\var{ec}$的乘积图（L12-13）。如果一个$\var{ec}$未通过可达性测试，则报告一个错误，表示无法满足该要求。处理完所有当前等价类后，拆分的等价类将从$\var{ecTable}$中移除（L17-18）。

\textbf{处理任播（Anycast）和多播（Multicast）。} 算法~\ref{alg:early-reg} 主要适用于单播流量，即乘积图中只有一个接受状态。当网络需求涉及任播或多播时，一个乘积图会有一组$K$个目的地（即接受状态）。在这种情况下，算法~\ref{alg:early-reg} 的第17行需要做出修改。对于任播，给定一个源节点 $src$，在$K$个 $Reachable(src, dst)$ 查询中，必须有且仅有一个返回 true，否则，将提前发现错误。对于多播，给定一个源节点 $src$，所有 $K$ 个 $Reachable(src, dst)$ 查询都必须返回 true，否则，将提前发现错误。

\textbf{验证路径覆盖需求。} 算法~\ref{alg:early-reg} 主要关注“存在性”要求，即满足正则表达式的有效路径必须存在。另一类重要的要求是“覆盖性”要求，即满足正则表达式的所有路径必须都存在~\cite{lopes2015checking}。这类要求的一个例子是Azure中的“所有冗余最短路径都应该可用”的需求~\cite{lopes2015checking}。CE2D通过首先基于正则表达式构建乘积图，然后进行覆盖性要求的提前验证，检查乘积图中的每个节点是否在任何时间都具有将数据包转发到其所有邻居节点的FIB，如果不满足，则提前发现错误。

\begin{algorithm}[t]
  \caption{针对正则表达式类型的需求验证算法}
  \label{alg:early-reg}
  % \small
  % \footnotesize
  \SetAlgoLined
  \SetKwInOut{Input}{Input}
  \SetKwInOut{Output}{Output}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKw{Abort}{abort}
  \SetKw{Not}{~not~}

  \textbf{Initialization}: $\var{ecTable} = \{H \mapsto
  \FuncSty{CreateProductGraph}{(G, \var{rexpr}, \var{Port}_{\var{in}})}\}$\;
  \Fn{\FuncSty{ConsistentPartialVerification}{($\var{ctx}$)}}{
    $\var{EC} \gets \FuncSty{GetEC}{(\var{ctx}.M)}$\;
    $\Delta \var{sync} \gets \var{ctx}.\var{sync} \setminus \var{sync}$\;
    $\var{sync} \gets \var{ctx}.\var{sync}$,
    $D \gets \emptyset$\;
    \ForEach{$\var{ec} \in \{\var{ec} \in \var{EC} \mid \var{ec} \cap H \neq \emptyset\}$}{
      \If{$\var{ec} \notin \var{ecTable}$}{
        $(\var{ec}^\prime, G_P^\prime) \gets \FuncSty{FindEntryToSplit}{(\var{ecTable})}$\;
        $\var{ecTable}[\var{ec}] \gets G_P$\;
        $D \gets D \cup \{\var{ec}^\prime\}$\;
      }
      $G_P\gets \var{ecTable}[\var{ec}]$\;
      \ForEach{$v \in \Delta\var{sync}$}{
        $G_P \gets \FuncSty{PruneIncompatibleEdges}{(G_P, \var{ec}, v)}$\;
      }
      $\var{ecTable}[\var{ec}] \gets G_P$\;
      \If{\Not $\FuncSty{Reachable}{(\var{ec}, G_P)}$}{
        \Return \emph{Unsatisfied}
      }
    }
    \ForEach{$\var{ec}^\prime \in D$}{
      $\FuncSty{Delete}{\var{ecTable}[\var{ec}^\prime]}$\;
    }
    \Return \emph{UNKNOWN}
  }
\end{algorithm}

\subsection{针对网络环路检测的数据平面需求增量式验证}
网络环路检测是数据平面验证中的一个常见的基本任务。然而，表达环路检测需要复杂的正则表达式，因此效率较低。因此，本文设计了一个专门的CE2D算法来检测环路。一种简单的方法是删除未同步的节点，然后检查同步节点中是否存在环路，但是这种简单的方法在某些情况下可能会错过提前验证的机会。另一种方法是保留未同步的节点，但假设未同步的节点可以选择任意可能的下一跳，并枚举所有组合，这可能会导致计算开销很大。为了兼具两种方法的优点，CE2D引入了一种称为\textbf{hyper node 压缩}方法。

具体来说，hyper node 压缩方法将未同步节点的每个连通分量压缩为一个超级节点，以减少枚举的数量。设$U$表示一个未同步节点的连通分量，将其替换为一个超级节点$w$。对于每个$(u, v) \in E$，其中$u \notin U$且$v \in U$，移除$(u, v)$并添加边$(u, w)$到$E$。在使用hyper node压缩的图上做验证得到的结果与在完整图上验证的结果相同，但避免了对$U$中路径的枚举。
\begin{figure}[htp]
  \centering
  \includegraphics[width=0.8\textwidth]{figures/consistency/hypernode.pdf}
  \caption{未同步节点压缩为hyper node}
  \label{fig:ld-example}
\end{figure}

% \begin{figure}[htp]
%   \centering
%   \includegraphics[width=0.5\textwidth]{consistency/example-aplf-3.pdf}
%   \caption{X is unsynchronized.}
%   \label{fig:ld-example1}
% \end{figure}

考虑图\ref{fig:ld-example} 中的示例，当$\var{sync} = \{A, B\}$时，可以将未同步节点$C$和$X$合并为一个超级节点，记为$C\&X$。在这种情况下，可能存在一个循环，例如$B \rightarrow A \rightarrow C\&X \rightarrow B$，在原始图中表示为$B \rightarrow A \rightarrow X \rightarrow B$，也可能不存在循环，例如$B \rightarrow A \rightarrow C\&X \rightarrow \var{out}$，在原始图中表示为$B \rightarrow A \rightarrow X \rightarrow C \rightarrow \var{out}$。因此，最终的结果无法确定。
然而，如果$C$是同步的，如\cref{fig:ld-example}中最右边所示，CE2D会报告如下结果：只要$X$不丢弃数据包~\footnote{在某些情况下，如访问控制列表（ACL），丢弃数据包被认为是可以接受的。在这种情况下，该算法只需要进行小的修改即可，即将明确的“DROP”操作视为转发到一个“虚拟交换机”。}，最终状态中将存在一个循环。如果只验证同步节点，则无法检测到这种情况。

\begin{theorem}
  如果数据平面模型$M_k$是一致性数据平面模型，令$ver_l$为基于hyper node压缩的循环验证函数，当$ver_l(M_k)$能够得到明确的结果，则$ver_l$实现了一致性提前验证。
\end{theorem}

\begin{proof}
  如果 $\var{ver}_l$ 不能实现一致的提前验证，那么根据~\cref{def:ced}，存在 $k' > k$ 使得 $\var{ver}_l(M_k) \neq \var{ver}_l(M_{k'})$。这意味着在应用了 $k'$ 次更新后，环路检测结果发生了变化。由于 $\var{ver}_l$ 仅检查同步节点之间的环路，打破环路的唯一方法是更新同步节点的 FIB。然而，$M_k$ 是一个保证在同步节点上没有更新的一致模型，因此不存在这样的 $k'$。
\end{proof}

\begin{algorithm}[h]
  \caption{一致性网络循环验证算法}
  \label{alg:cpld}
  \small
  \DontPrintSemicolon
  \SetKwInOut{Input}{Input}
  \SetKwInOut{Output}{Output}
  \SetKwProg{Fn}{Function}{}{}
  \SetKw{Continue}{continue}
  \SetKw{Abort}{abort}
  \SetKw{True}{~true~}
  \SetKw{False}{~false~}
  \SetKw{And}{~and~}
  \Fn{$\FuncSty{ConsistentPartialLoopDetect}{(\var{ctx})}$}{
    $G_{\var{hyper}} \gets \FuncSty{BuildHyperGraph}{(G, \var{ctx}.\var{sync})}$\;
    $\Delta \var{sync} \gets \var{ctx}.\var{sync} \setminus \var{sync}$\;
    $\var{sync} \gets \var{ctx}.\var{sync}$,
    $\var{potentialResults} \gets \emptyset$\;
    \For{$v \in \Delta\var{sync}$}{
      $\var{results} \gets \FuncSty{DetectLoop}{(v, \{\var{ec} \in \var{ctx}.M\},
        \emptyset, \text{\textbf{false}})}$\;
      \If{a deterministic loop is found}{
        \Return $\{\var{Loop}\}$\;
      }
      $\var{potentialResults} \gets \var{potentialResults} \cup \var{results}$\;
    }
    \Return $\var{potentialResults}$\;
  }
  \Fn{\FuncSty{DetectLoop}{($v,\var{EC},\var{path},\var{hyper}$)}}{
    \If{$\var{EC} = \emptyset$}{
      \Return $\emptyset$\;
    }
    $\var{potentialResults} \gets \emptyset$\;
    \If{$v$ is external}{
      \Return $\{\var{NoLoop}\}$
    }\ElseIf{$v.\var{is\_hyper}$\And$v.\var{is\_biconnected}$}{
      $\var{potentialResults} \gets \var{potentialResults} \cup \{\var{Loop}\}$\;
    }\ElseIf{$v \in \var{path}$\And$\var{hyper} = \True$}{
      \Return $\{\var{Loop}\}$\;
    }\ElseIf{$v \in \var{path}$\And$\var{hyper} = \False$}{
      \Abort \emph{Loop}
    }
    \ForEach{$(v, u) \in G_{\var{hyper}}$}{
      $\var{validEC} \gets \var{EC} \cap \var{EC}(v, u)$,
      $\var{path}^\prime \gets \var{path} \cup \{v\}$\;
      $r \gets \FuncSty{DetectLoop}{(u, \var{validEC},
        \var{path}^\prime, \var{hyper}\vee{u.\var{hyper}})}$\;
      $\var{potentialResults} \gets \var{potentialResults} \cup r$\;
    }
    \Return $\var{potentialResults}$\;
  }
\end{algorithm}

\paragraph{CE2D针对网络环路的增量检测。}
CE2D只检测包含最新的变为同步节点的循环，而不是从所有可能的节点中检测循环。设$V_S$和$V_S'$分别表示旧的和新的同步节点集合。
如果在旧图中没有检测到循环，那么在新图中出现的新循环必定包含$V_S' - V_S$中的节点。结合hyper node抽象和增量检测，CE2D逐步检查新的同步节点。如果发现由仅包含同步节点构成的循环，则报告错误。代码~\ref{alg:cpld} 给出了具体的伪代码。它首先构建hyper node图（L2），然后开始检测循环（L6）。如果发现确定性循环，即只包含同步节点的循环（L7-8，L22），它会给出关于循环的一致提前验证结果。检测函数验证以$v$为最后一个节点的路径，对于一组等价类$\var{EC}$。$\var{path}$表示不包含$v$的路径段，$\var{hyper}$表示路径中是否包含超级节点。检测方法检查各种条件（L15-22）以确定路径的结果是否已知。如果不知道，它会将路径延伸到每个潜在的下一跳$u$，针对能够从$v$到$u$的路径接受路径的潜在等价类（L24），并收集这些延伸路径的所有潜在结果（L25-26）。

\section{实验设计和结果分析}
\label{sec:ce2d-eval}
为了评估CE2D实现一致性提前验证的效果，实验采用了真实网络拓扑和真实数据集，并通过实验主要回答以下问题：
\begin{enumerate}
  \item CE2D是否能够实现一致性提前验证？
  \item CE2D的增量式验证方法是否能够实现快速验证？
\end{enumerate}

\subsection{系统实现}
CE2D被设计为Flash的验证组件和数据平面更新分发组件，使用约1,100行Java代码实现。其中数据平面分发组件通过读取数据平面更新的纪元标签对数据平面更新进行分组，然后将每个分组的数据平面更新发送到相应的Flash数据平面模型构建组件，形成一致性数据平面模型集合。在进行网络需求验证时，CE2D基于JGraphT~\cite{jgrapht}实现递减图查询结构，并在数据平面模型发生更新时自动触发增量式验证过程。

\subsection{CE2D实现一致性提前验证效果评估}
首先对CE2D是否能够实现一致性验证进行评估，实验在真实路由软件OpenR实例构建的网络拓扑下进行，具体实验设计如下：

\textbf{实验设计。}
验证CE2D能否提供一致的提前验证结果实验设计如下。使用Mininet~\cite{lantz2010network}构建了一个与Internet2拓扑结构一致的网络。每个设备上都运行了一个真实的OpenR实例。通过连续失效两个链路（chic-alta和chic-kans）来触发FIB更新。实验将CE2D与以下两种策略进行比较：
\begin{enumerate}
\item 每次更新验证（PUV），它在处理单个规则更新后检查属性（例如，HSA~\cite{kazemian2012header}、APKeep~\cite{zhang2020apkeep}和DeltaNet~\cite{horn2017deltanet}）。
\item 块更新验证（BUV），它在处理一组更新后进行验证（例如，DNA~\cite{zhang2022differential}）。
\end{enumerate}

\textbf{实验结果。}
实验在验证器上记录了每个交换机的FIB更新时间以及验证器报告确定性结果的时间。结果如图~\ref{fig:eval-i2-openr-arrival}所示。十字点$(x，y)$表示交换机$y$的FIB更新在自链路故障触发后的时间$x$收到，颜色表示纪元标签。点$(x, y)$表示验证器策略$y$在时间$x$报告了确定性结果，其中橙色表示存在环路，蓝色表示不存在环路。如结果所示，两个同时发生的链路故障在每个交换机上触发多次FIB重新计算。使用PUV和BUV，验证器报告了两个短暂的环路（橙色点），这与最终验证结果不一致。同时，系统不报告误报错误，并保证验证结果是一致的。

\begin{figure}[htp]
  \centering
  \includegraphics[width=0.65\textwidth]{CE2D-OpenR-consistent.pdf}
  \caption{FIB更新和验证报告的时间分布图}
  \label{fig:eval-i2-openr-arrival}
\end{figure}

% \subsection{长尾到达情况下的CE2D效果评估}
为了验证CE2D在“长尾到达”情况下是否能够实现一致性提前验证，实验根据真实数据集和拓扑构建，具体实验设计如下：

\textbf{实验设计。}
在发生环路的两种设置下评估了CE2D在“长尾到达”情况下的效果：1）\evalSettingOpenrsLT：基于真实OpenR实例构建Internet2拓扑，其中一个OpenR设备计算FIB出错；2）\evalSettingILT：基于Internet2真实数据集构建其网络拓扑，配置其中部分网络设备FIB计算时间阻尼为默认的60秒。对于每个实验设置，进行了50次独立的随机试验，在\evalSettingOpenrsLT 设置的每次试验中，通过配置一个随机节点延迟60秒发送更新来模拟长尾效应，测量并记录了 CE2D 报告确定性结果的时间。

另外，设计了实验以评估网络中在存在多个设备发生延迟更新时CE2D的效果。实验使用\evalSettingILT 的数据集，采用来自Internet2数据集的真实网络拓扑和更新序列。从1到7枚举阻尼设备的数量$D$。对于每个$D$，使用CE2D检查环路，并进行50次独立的随机试验。

\textbf{实验结果。}
结果如\cref{fig:eval-openr-loop-time-cdf}所示。横轴表示报告时间，纵轴表示累积分布函数（CDF）。横轴范围限定在[0ms, 1,000ms]：如果一条曲线在1,000ms时未达到y=1，则表示结果在60秒后获得，即在收到发生长尾更新节点的更新之后。从图中可以看出，\evalSettingOpenrsLT 曲线上的点 (153.7ms, 0.68) 表明在68\%的试验中，CE2D 可以在不到153.7ms内检测到环路，这比60秒的基准时间小得多（>390倍）。在\evalSettingILT 中，CE2D 可以在所有试验中在不到760ms内提前验证到环路，速度提升了79倍。因此，实验得出结论：在“长尾到达”的情况下，CE2D在大部分情况下（68\%至100\%）能够提前得到一致的验证结果，且速度提升显著（79倍至>390倍）。

对于多个设备发生阻尼的情况，图\ref{fig:eval-i2-time-cdf} 显示了CE2D的效果。在所有情况中，有72.5\%（即145/200）的情况下，CE2D可以在800毫秒内检测到一致的环路，速度比完整验证快75倍。随着阻尼设备数量$D$的增加，成功进行一致提前验证的概率变得较低。例如，当$D \leq 3$时，CE2D仍然可以在超过90\%的情况下在800毫秒内检测到错误，当$D=7$时，即77.8\%的交换机被阻尼时，在约20\%的情况下仍然能够在800毫秒内检测到错误。因此，实验得出结论：即使只有有限和部分的数据平面更新信息，CE2D仍然可以提前得到一致的验证结果。

\begin{figure}[htp]
  \centering
  \includegraphics[width=0.65\textwidth]{consistency/CE2D-1buggy-lt.pdf}
  \caption{CE2D验证结果报告时间}
  \label{fig:eval-openr-loop-time-cdf}
\end{figure}

\begin{figure}[htp]
  \centering
  \includegraphics[width=0.65\textwidth]{consistency/dampened.pdf}
  \caption{CE2D在不同数量设备发生更新延迟的验证报告时间}
  \label{fig:eval-i2-time-cdf}
\end{figure}

\subsection{CE2D的增量式验证效果评估}

\textbf{实验设计。}
为了评估CE2D的增量式验证效果，实验通过使用递减验证图方法对基于正则表达式的需求执行一致提前验证。实验使用LNet-apsp Subspace设置（参见\cref{sec:model-eval}）并检查所有对ToR到ToR的可达性。Flash总共生成5,376个验证图，每个子空间验证器生成48个验证图。每个交换机的规则插入都作为一个批处理输入Flash。Flash在处理每个批次后验证可达性，并使用1）递减图查询（DGQ）方法和 2）模型遍历（MT，即使用深度优先遍历从每个源ToR遍历模型）来测量单个子空间验证器的验证执行时间。

\textbf{实验结果。}
图~\ref{fig:eval-cdf-auto-allpair} 显示了验证时间的CDF。可以看到，DGQ（蓝色）比MT（橙色）更靠近y轴。DGQ和MT的中位数、平均值、99\%和最长时间分别为0.58/0.84/4.74/19.57ms和772.98/1,522.22/5,513.76/7,466.87ms。与MT相比，Flash将99\%的执行时间提高了约1,163倍（5513.76ms/4.74ms）。因此，可以得出结论，递减验证图方法大大提高了基于正则表达式的需求的验证性能，并实现了高效一致的提前验证。

\begin{figure}[]
  \center
  \includegraphics[width=0.65\textwidth]{allpair.pdf}
  \caption{对ToR-to-ToR可达性检查的执行时间}
  \label{fig:eval-cdf-auto-allpair}
\end{figure}

除了上述结果外，实验还获取了验证时间随着处理的更新数量的增加而变化过程。结果如图~\ref{fig:allpair-update}所示。MT的验证时间随着更多规则更新的完成而增加，而这种趋势在DGQ方法中没有表现出来。原因是模型遍历的计算复杂度为$O(|V|\times(|V|+|E|))$, 并且随着更多的规则更新完成$|E|$ 正在增加。而DGQ在开始时计算验证图的连通分量，其复杂性为$O(|V| + |E|)$, 且$|E|$ 随着更多设备更新的完成而减少。

\begin{figure}[]
  \center
  \includegraphics[width=0.65\textwidth]{allpair-update.pdf}
  \caption{处理不同数量的更新后的验证时间}
  \label{fig:allpair-update}
\end{figure}




\section{本章小结}
本章针对大规模网络的数据平面一致性快速验证进行研究。对于大规模网络中存在的“长尾到达”现象，分析了“长尾到达”现象所涉及的完成状态不确定性和数据平面更新异步性等挑战。然后，提出了一种专为大规模网络设计的数据平面一致性快速验证方法CE2D。作为Flash验证过程的核心组成部分，CE2D将数据平面更新分为不同的纪元，并引入了一种创新的基于递减图查询的增量式验证方法。最后，实验表明CE2D相比已有工作能够提高升1,163倍的验证速度。